A, C:Type, B:(AType), eqa:EqDecider(A), eqc:EqDecider(C), r:(AC), f:a:A fp B(a), a:A.
Inj(A;C;r)  (a  dom(f))  (rename(r;f)(r(a)) = f(a)  B(a)) 

latex

Definitions	x:A. B(x), x(s), P  Q, f(x), rename(r;f), t.2, t.1, t  T, x. t(x), x:A. B(x), P & Q, , P  Q, P  Q, a:A fp B(a), x  dom(f), A c B, Inj(A;B;f)
Lemmas	hd-filter, eqof wf, assert wf, fpf-dom wf, fpf-trivial-subtype-top, inject wf, fpf wf, deq wf, l member wf, assert-deq-member, deq property, subtype rel self